Commentary by Chris Pressey
===========================

<!--
Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.

SPDX-License-Identifier: CC-BY-ND-4.0
-->

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
exception: the ratings may be freely used for any purpose with no limitations.

Proof Theory
---------------

### Basic Proof Theory

*   rating: TODO

.

### A Paedagogic Example of Cut-Elimination

*   rating: 1

The author notes that it was a very deep insight of Gentzen's that classical logic
is symmetric between true and false, and this is reflected in the sequent calculus:
either what's to left of the turnstile is false, or what's to the right is true.

LI is a cute little theory, but as far as I can tell it's quite weak; the theory
of lattices with inequality.  Still, it is simple and you can prove some things in it:
for example, a weak distributivity law.